old_event_system{i:l}()
== E:Type
== EqDecider(E)
== T:(IdIdType)
== V:(IdIdType)
== M:(IdLnkIdType)
== Top
== loc:(EId)
== kind:(EKnd)
== val:(e:Eeventtype(kind;loc;V;M;e))
== when:(x:Ide:ET(loc(e),x))
== after:(x:Ide:ET(loc(e),x))
== sends:(l:IdLnkE(Msg_sub(l;M) List))
== sender:({e:E| isrcv(kind(e)) }E)
== index:(e:{e:E| isrcv(kind(e)) }||sends(lnk(kind(e)),sender(e))||)
== first:(E)
== pred:({e':E| first(e') }E)
== causl:(EEProp)
== ESAxioms(E;T;M;
== ESAxioms(loc;kind;val;
== ESAxioms(when;after;
== ESAxioms(sends;sender;index;
== ESAxioms(first;pred;
== ESAxioms(causl)
== Trans:(i:Idk:Kndkindcase(k; a.V(i,a); l,t.M(l,t) )(x:IdT(i,x))(x:IdT(i,x)))
== Send:(i:Idk:Kndkindcase(k; a.V(i,a); l,t.M(l,t) )(x:IdT(i,x))(Msg(M) List))
== Choose:(i,a:Id(x:IdT(i,x))(V(i,a)+Unit))
== ESMachineAxiom(E;T;V;M;loc;kind;val;
== when;after;
== sender;Trans;Send;Choose)
== ESAtomAxiom{i:l}(T;i,k. kindcase(k; a.V(i,a); l,t.M(l,t) ))
== Top 

latex

---

clarification:

old_event_system{i:l}
== E:Type{i}
== EqDecider(E)
== T:(IdIdType{i})
== V:(IdIdType{i})
== M:(IdLnkIdType{i})
== Top
== loc:(EId)
== kind:(EKnd)
== val:(e:Eeventtype(kind;loc;V;M;e))
== when:(x:Ide:ET(loc(e),x))
== after:(x:Ide:ET(loc(e),x))
== sends:(l:IdLnkE(Msg_sub(l;M) List))
== sender:({e:E| isrcv(kind(e)) }E)
== index:(e:{e:E| isrcv(kind(e)) }{0..||sends(lnk(kind(e)),sender(e))||})
== first:(E)
== pred:({e':E| first(e') }E)
== causl:(EEProp{i})
== ESAxioms{i:l}
== ESAxioms(E; T; M; loc; kind; val; when; after; sends; sender; index; first; pred; causl)
== Trans:(i:Idk:Kndkindcase(k; a.V(i,a); l,t.M(l,t) )(x:IdT(i,x))(x:IdT(i,x)))
== Send:(i:Idk:Kndkindcase(k; a.V(i,a); l,t.M(l,t) )(x:IdT(i,x))(Msg(M) List))
== Choose:(i:Ida:Id(x:IdT(i,x))(V(i,a)+Unit))
== ESMachineAxiom(E;T;V;M;loc;kind;val;
== when;after;
== sender;Trans;Send;Choose)
== ESAtomAxiom{i:l}
== ESAtomAxiom(T; (i,k. kindcase(k; a.V(i,a); l,t.M(l,t) )))
== Top 

latex

Definitions

EqDecider(T), Type, eventtype(k;loc;V;M;e), IdLnk, Msg_sub(l;M), isrcv(k), {i..j}, #$n, ||as||, lnk(k), , {x:A| B(x) }, A, b, Prop, ESAxioms(E;T;M;loc;kind;val;when;after;sends;sender;index;first;pred;causl), Knd, type List, Msg(M), x:AB(x), Id, left+right, Unit, ESMachineAxiom(E;T;V;M;loc;knd;val;when;after;sndr;Trans;Send;Choose), x:AB(x), ESAtomAxiom{i:l}(T;V), x.A(x), kindcase(k; a.f(a); l,t.g(l;t) ), f(a), Top

FDL editor aliases

old_event_system